A, B, C:MsgA.
A || B  ma-frame-compat(A;C)  ma-frame-compat(B;C)  ma-frame-compat(A  B;C) 

latex

Definitions

x:A. B(x), P  Q, t  T, M1  M2, Prop, 1of(t), 2of(t), P  Q, mk-ma, x. t(x), ma-frame-compat(A;B), P & Q, xdom(f). v=f(x)   P(x;v), M.rframe(A.pre p for a), M.frame(k affects x), M.aframe(k affects x), M.rframe(A.effect f of k on y), M.sframe(k sends <l,tg>), M.bframe(k sends on l), M.rframe(A.sends tfL of k on l), M.state, M.da(a), (s1  s2 mod x), M.dout(l,tg), M.ds(x), P  Q, {T}, P  Q, M1 || M2, MsgA, x(s), M1  M2, Valtype(da;k), A & B, f  g, State(ds)

Lemmas

ma-join wf, ma-frame-compat wf, ma-compatible wf, msga wf, ma-sub-join-left, ma-sub wf, ma-sub-join-right, fpf-join-dom-sq, assert of bor, fpf-dom wf, assert wf, Id wf, id-deq wf, fpf-join wf, top wf, fpf-trivial-subtype-top, ma-state wf, ma-valtype wf, locl wf, Knd wf, product-deq wf, Kind-deq wf, pi1 wf, fpf-cap wf, pi2 wf, IdLnk wf, idlnk-deq wf, rcv wf, ma-state-subtype, subtype-fpf-cap-top, not wf, iff wf, fpf-ap wf, deq-member wf, subtype-fpf-cap-void